{
module LanguageParser(parseString) where
import LanguageLexer
import Synchronizers
import LanguageDef
}

%name monadParse
%tokentype { Token }
%monad { Alex }
%lexer { languageLexer } { EOFToken }

%token
    INTEGER     { Token (IntegerConst _) _ }
    STRING      { Token (StringConst _) _ }
    TRUE        { Token (TrueConst) _ }
    FALSE       { Token (FalseConst) _ }
    NULL        { Token (NullConst) _ }
    NAME        { Token (Name _) _ }
    '('         { Token (Operator "(") _ }
    ')'         { Token (Operator ")") _ }
    '->'        { Token (Operator "->") _ }
    '='         { Token (Operator "=") _ }
    ':='        { Token (Operator ":=") _ }
    ','         { Token (Operator ",") _ }
    '.'         { Token (Operator ".") _ }
    '|'         { Token (Operator "|") _ }
    AND         { Token (Keyword "and") _ }
    OR          { Token (Keyword "or") _ }
    FORALL      { Token (Keyword "forall") _}
    EXISTS      { Token (Keyword "exists") _}
    EXISTSE     { Token (Keyword "exists!") _}
    LET         { Token (Keyword "let") _}
    IN          { Token (Keyword "in") _}
    PROTECT     { Token (Keyword "protect") _}
    TEST        { Token (Keyword "test") _}
    NOT         { Token (Keyword "not") _}
    DEF         { Token (Keyword "def") _}
    TRACE       { Token (Keyword "trace") _}
    ONE         { Token (Keyword "one") _}
    OF          { Token (Keyword "of") _}
    PRINTING    { Token (Keyword "printing") _}
    
%left OR
%left AND
%left TRACE 
%right PRINTING OF
%left NOT TEST IN
%left '='
%left '->'
%left '.'
	
%%
program :: {Node}
program : decls {Node RootNode (Pos 0 0) $1}

decls :: { [Node]}
decls : decl    { [$1] }
      | decl decls {$1:$2}
      
decl :: {Node}
decl : DEF NAME '(' arg_list ')' ':=' cstraint { Node (RelationDefNode $ getString $2) (getPos $1) [$4, $7] }

arg_list :: { Node }
arg_list : var_list { Node VarListNode (Pos 0 0) $1 }

var_list :: { [Node] }
var_list : var { [$1] }
         | var ',' var_list {$1:$3}
         
var :: { Node }
var : NAME { Node (VarNode (getString $1)) (getPos $1) []}

cstraint :: { Node }
cstraint : cstraint AND cstraint {Node AndNode (getPos $2) [$1, $3]}
         | cstraint OR cstraint  {Node OrNode (getPos $2) [$1, $3]}
         | expr '=' expr {Node EqualNode (getPos $2) [$1, $3]}
         | expr '->' FORALL '(' var '|' cstraint ')' { Node ForAllNode (getPos $3) [$1, $5, $7] }
         | expr '->' EXISTS '(' var '|' cstraint ')' { Node ExistsNode (getPos $3) [$1, $5, $7] }
         | expr '->' EXISTSE '(' var '|' cstraint ')' { Node Exists'Node (getPos $3) [$1, $5, $7] }
         | expr '->' ONE '(' var '|' cstraint ')' { Node OneNode (getPos $3) [$1, $5, $7] }
         | expr '=' expr '->' ONE '(' var '|' cstraint ')' { Node One'Node (getPos $5) [$1, $3, $7, $9] }
         | LET var '=' expr IN cstraint { Node LetNode (getPos $1) [$2, $4, $6] }
         | PROTECT var IN cstraint { Node ProtectNode (getPos $1) [$2, $4] }
         | TEST cstraint { Node TestNode (getPos $1) [$2] }
         | NOT cstraint { Node NotNode (getPos $1) [$2] }
         | '(' cstraint ')' { $2 }
         | NAME '(' expr_list ')' { Node (RelationRefNode $ getString $1) (getPos $1) $3 }
         | TRACE cstraint  optionalArgs optionalMsg { Node (CTraceNode $ $4 ++ pos2String (getNodePos $2) "" ) (getPos $1) [$3, $2]  } 

optionalMsg :: {String}
optionalMsg : PRINTING STRING %prec PRINTING {"\"" ++ getString $2 ++ "\""}
        | %prec PRINTING{""}
        
optionalArgs :: {Node}
optionalArgs : OF '(' arg_list ')' %prec OF {$3}
        | OF '(' ')' %prec OF {Node VarListNode (Pos 0 0) []}
        | %prec OF {Node AllVarNode (Pos 0 0) []}
         
expr :: {Node}
expr : var {$1}
     | TRACE expr optionalArgs optionalMsg { Node (ETraceNode $ $4 ++ pos2String (getNodePos $2) "" ) (getPos $1) [$3, $2]  } 
     | '(' expr ')' {$2}
     | expr '.' expr {Node DictGetNode (getPos $2) [$1, $3]}
     | const {Node IsConstNode ((\(Node _ pos _)->pos) $1) [$1]}
     
expr_list :: { [Node] }
epxr_list : expr { [$1] }
         | expr ',' expr_list {$1:$3}
     
const :: {Node}
const : STRING { Node (StringConstNode $ getString $1) (getPos $1) []}
      | INTEGER { Node (IntConstNode $ getInt $1) (getPos $1) []}
      | FALSE  { Node (StringConstNode "@false") (getPos $1) []}
      | TRUE  { Node (StringConstNode "@true") (getPos $1) []}
      | NULL  { Node (NullConstNode ) (getPos $1) []}



{

getString :: Token -> String
getString (Token (StringConst s) _) = s  
getString (Token (Name s) _) = s  
getString (Token (Operator s) _) = s  
getString (Token (Keyword s) _) = s  
getString _ = ""  

getInt :: Token -> Int
getInt (Token (IntegerConst i) _) = i
getInt _ = 0


happyError :: Alex a
happyError = do
	line <- alexGetLine
	column <- alexGetColumn
	alexError ("line " ++ show line ++ ", column " ++ show column ++": parser error")
	
parseString :: String -> Either String Node
parseString input = runAlex input monadParse
	

}